diff options
author | Florian Dold <florian.dold@gmail.com> | 2019-03-27 21:01:33 +0100 |
---|---|---|
committer | Florian Dold <florian.dold@gmail.com> | 2019-03-27 21:01:33 +0100 |
commit | cc97a4dd2a967e1c2273bd5f4c5f49a5bf2e2585 (patch) | |
tree | 92c5d88706a6ffc654d1b133618d357890e7096b /node_modules/highlight.js/lib/languages/coq.js | |
parent | 3771b4d6b67b34c130f3a9a1a15f42deefdb2eda (diff) |
remove node_modules
Diffstat (limited to 'node_modules/highlight.js/lib/languages/coq.js')
-rw-r--r-- | node_modules/highlight.js/lib/languages/coq.js | 66 |
1 files changed, 0 insertions, 66 deletions
diff --git a/node_modules/highlight.js/lib/languages/coq.js b/node_modules/highlight.js/lib/languages/coq.js deleted file mode 100644 index 0744ac6cd..000000000 --- a/node_modules/highlight.js/lib/languages/coq.js +++ /dev/null @@ -1,66 +0,0 @@ -module.exports = function(hljs) { - return { - keywords: { - keyword: - '_ as at cofix else end exists exists2 fix for forall fun if IF in let ' + - 'match mod Prop return Set then Type using where with ' + - 'Abort About Add Admit Admitted All Arguments Assumptions Axiom Back BackTo ' + - 'Backtrack Bind Blacklist Canonical Cd Check Class Classes Close Coercion ' + - 'Coercions CoFixpoint CoInductive Collection Combined Compute Conjecture ' + - 'Conjectures Constant constr Constraint Constructors Context Corollary ' + - 'CreateHintDb Cut Declare Defined Definition Delimit Dependencies Dependent' + - 'Derive Drop eauto End Equality Eval Example Existential Existentials ' + - 'Existing Export exporting Extern Extract Extraction Fact Field Fields File ' + - 'Fixpoint Focus for From Function Functional Generalizable Global Goal Grab ' + - 'Grammar Graph Guarded Heap Hint HintDb Hints Hypotheses Hypothesis ident ' + - 'Identity If Immediate Implicit Import Include Inductive Infix Info Initial ' + - 'Inline Inspect Instance Instances Intro Intros Inversion Inversion_clear ' + - 'Language Left Lemma Let Libraries Library Load LoadPath Local Locate Ltac ML ' + - 'Mode Module Modules Monomorphic Morphism Next NoInline Notation Obligation ' + - 'Obligations Opaque Open Optimize Options Parameter Parameters Parametric ' + - 'Path Paths pattern Polymorphic Preterm Print Printing Program Projections ' + - 'Proof Proposition Pwd Qed Quit Rec Record Recursive Redirect Relation Remark ' + - 'Remove Require Reserved Reset Resolve Restart Rewrite Right Ring Rings Save ' + - 'Scheme Scope Scopes Script Search SearchAbout SearchHead SearchPattern ' + - 'SearchRewrite Section Separate Set Setoid Show Solve Sorted Step Strategies ' + - 'Strategy Structure SubClass Table Tables Tactic Term Test Theorem Time ' + - 'Timeout Transparent Type Typeclasses Types Undelimit Undo Unfocus Unfocused ' + - 'Unfold Universe Universes Unset Unshelve using Variable Variables Variant ' + - 'Verbose Visibility where with', - built_in: - 'abstract absurd admit after apply as assert assumption at auto autorewrite ' + - 'autounfold before bottom btauto by case case_eq cbn cbv change ' + - 'classical_left classical_right clear clearbody cofix compare compute ' + - 'congruence constr_eq constructor contradict contradiction cut cutrewrite ' + - 'cycle decide decompose dependent destruct destruction dintuition ' + - 'discriminate discrR do double dtauto eapply eassumption eauto ecase ' + - 'econstructor edestruct ediscriminate eelim eexact eexists einduction ' + - 'einjection eleft elim elimtype enough equality erewrite eright ' + - 'esimplify_eq esplit evar exact exactly_once exfalso exists f_equal fail ' + - 'field field_simplify field_simplify_eq first firstorder fix fold fourier ' + - 'functional generalize generalizing gfail give_up has_evar hnf idtac in ' + - 'induction injection instantiate intro intro_pattern intros intuition ' + - 'inversion inversion_clear is_evar is_var lapply lazy left lia lra move ' + - 'native_compute nia nsatz omega once pattern pose progress proof psatz quote ' + - 'record red refine reflexivity remember rename repeat replace revert ' + - 'revgoals rewrite rewrite_strat right ring ring_simplify rtauto set ' + - 'setoid_reflexivity setoid_replace setoid_rewrite setoid_symmetry ' + - 'setoid_transitivity shelve shelve_unifiable simpl simple simplify_eq solve ' + - 'specialize split split_Rabs split_Rmult stepl stepr subst sum swap ' + - 'symmetry tactic tauto time timeout top transitivity trivial try tryif ' + - 'unfold unify until using vm_compute with' - }, - contains: [ - hljs.QUOTE_STRING_MODE, - hljs.COMMENT('\\(\\*', '\\*\\)'), - hljs.C_NUMBER_MODE, - { - className: 'type', - excludeBegin: true, - begin: '\\|\\s*', - end: '\\w+' - }, - {begin: /[-=]>/} // relevance booster - ] - }; -};
\ No newline at end of file |