From 420f78b2caeaaddc6fe484565b2d0e49c66888e5 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Sun, 27 Jul 2014 10:02:38 +0200 Subject: Imported Upstream version 8.4pl4dfsg --- plugins/cc/ccalgo.ml | 2 +- plugins/cc/ccalgo.mli | 2 +- plugins/cc/ccproof.ml | 2 +- plugins/cc/ccproof.mli | 2 +- plugins/cc/cctac.ml | 2 +- plugins/cc/cctac.mli | 2 +- plugins/cc/g_congruence.ml4 | 2 +- plugins/decl_mode/decl_expr.mli | 2 +- plugins/decl_mode/decl_interp.ml | 2 +- plugins/decl_mode/decl_interp.mli | 2 +- plugins/decl_mode/decl_mode.ml | 2 +- plugins/decl_mode/decl_mode.mli | 2 +- plugins/decl_mode/decl_proof_instr.ml | 2 +- plugins/decl_mode/decl_proof_instr.mli | 2 +- plugins/decl_mode/g_decl_mode.ml4 | 2 +- plugins/decl_mode/ppdecl_proof.ml | 2 +- plugins/extraction/ExtrOcamlBasic.v | 2 +- plugins/extraction/ExtrOcamlBigIntConv.v | 2 +- plugins/extraction/ExtrOcamlIntConv.v | 2 +- plugins/extraction/ExtrOcamlNatBigInt.v | 2 +- plugins/extraction/ExtrOcamlNatInt.v | 2 +- plugins/extraction/ExtrOcamlString.v | 2 +- plugins/extraction/ExtrOcamlZBigInt.v | 2 +- plugins/extraction/ExtrOcamlZInt.v | 2 +- plugins/extraction/big.ml | 2 +- plugins/extraction/common.ml | 2 +- plugins/extraction/common.mli | 2 +- plugins/extraction/extract_env.ml | 2 +- plugins/extraction/extract_env.mli | 2 +- plugins/extraction/extraction.ml | 2 +- plugins/extraction/extraction.mli | 2 +- plugins/extraction/g_extraction.ml4 | 2 +- plugins/extraction/haskell.ml | 2 +- plugins/extraction/haskell.mli | 2 +- plugins/extraction/miniml.mli | 2 +- plugins/extraction/mlutil.ml | 2 +- plugins/extraction/mlutil.mli | 2 +- plugins/extraction/modutil.ml | 2 +- plugins/extraction/modutil.mli | 2 +- plugins/extraction/ocaml.ml | 2 +- plugins/extraction/ocaml.mli | 2 +- plugins/extraction/scheme.ml | 2 +- plugins/extraction/scheme.mli | 2 +- plugins/extraction/table.ml | 2 +- plugins/extraction/table.mli | 2 +- plugins/field/LegacyField.v | 2 +- plugins/field/LegacyField_Compl.v | 2 +- plugins/field/LegacyField_Tactic.v | 2 +- plugins/field/LegacyField_Theory.v | 2 +- plugins/field/field.ml4 | 2 +- plugins/firstorder/formula.ml | 2 +- plugins/firstorder/formula.mli | 2 +- plugins/firstorder/g_ground.ml4 | 2 +- plugins/firstorder/ground.ml | 2 +- plugins/firstorder/ground.mli | 2 +- plugins/firstorder/instances.ml | 2 +- plugins/firstorder/instances.mli | 2 +- plugins/firstorder/rules.ml | 2 +- plugins/firstorder/rules.mli | 2 +- plugins/firstorder/sequent.ml | 2 +- plugins/firstorder/sequent.mli | 2 +- plugins/firstorder/unify.ml | 2 +- plugins/firstorder/unify.mli | 2 +- plugins/fourier/Fourier.v | 2 +- plugins/fourier/Fourier_util.v | 2 +- plugins/fourier/fourier.ml | 2 +- plugins/fourier/fourierR.ml | 2 +- plugins/fourier/g_fourier.ml4 | 2 +- plugins/funind/Recdef.v | 2 +- plugins/funind/functional_principles_proofs.ml | 6 +-- plugins/funind/g_indfun.ml4 | 2 +- plugins/funind/invfun.ml | 51 +++++++++++--------- plugins/funind/merge.ml | 2 +- plugins/funind/recdef.ml | 4 +- plugins/micromega/CheckerMaker.v | 2 +- plugins/micromega/Env.v | 2 +- plugins/micromega/EnvRing.v | 2 +- plugins/micromega/MExtraction.v | 2 +- plugins/micromega/OrderedRing.v | 2 +- plugins/micromega/Psatz.v | 2 +- plugins/micromega/QMicromega.v | 2 +- plugins/micromega/RMicromega.v | 2 +- plugins/micromega/Refl.v | 2 +- plugins/micromega/RingMicromega.v | 2 +- plugins/micromega/Tauto.v | 2 +- plugins/micromega/VarMap.v | 2 +- plugins/micromega/ZCoeff.v | 2 +- plugins/micromega/ZMicromega.v | 2 +- plugins/micromega/certificate.ml | 2 +- plugins/micromega/coq_micromega.ml | 34 +++++++------ plugins/micromega/csdpcert.ml | 2 +- plugins/micromega/g_micromega.ml4 | 2 +- plugins/micromega/mutils.ml | 2 +- plugins/micromega/persistent_cache.ml | 2 +- plugins/micromega/polynomial.ml | 2 +- plugins/micromega/sos.mli | 2 +- plugins/micromega/sos_types.ml | 2 +- plugins/nsatz/Nsatz.v | 2 +- plugins/nsatz/ideal.ml | 2 +- plugins/nsatz/nsatz.ml4 | 2 +- plugins/nsatz/polynom.ml | 2 +- plugins/nsatz/polynom.mli | 2 +- plugins/omega/Omega.v | 2 +- plugins/omega/OmegaPlugin.v | 2 +- plugins/omega/PreOmega.v | 2 +- plugins/omega/coq_omega.ml | 67 +++++++++++++++++++++----- plugins/omega/g_omega.ml4 | 2 +- plugins/omega/omega.ml | 2 +- plugins/quote/Quote.v | 2 +- plugins/quote/g_quote.ml4 | 2 +- plugins/quote/quote.ml | 2 +- plugins/ring/LegacyArithRing.v | 2 +- plugins/ring/LegacyNArithRing.v | 2 +- plugins/ring/LegacyRing.v | 2 +- plugins/ring/LegacyRing_theory.v | 2 +- plugins/ring/LegacyZArithRing.v | 2 +- plugins/ring/Ring_abstract.v | 2 +- plugins/ring/Ring_normalize.v | 2 +- plugins/ring/Setoid_ring.v | 2 +- plugins/ring/Setoid_ring_normalize.v | 2 +- plugins/ring/Setoid_ring_theory.v | 2 +- plugins/ring/g_ring.ml4 | 2 +- plugins/ring/ring.ml | 2 +- plugins/rtauto/Bintree.v | 2 +- plugins/rtauto/Rtauto.v | 2 +- plugins/rtauto/g_rtauto.ml4 | 2 +- plugins/rtauto/proof_search.ml | 2 +- plugins/rtauto/proof_search.mli | 2 +- plugins/rtauto/refl_tauto.ml | 2 +- plugins/rtauto/refl_tauto.mli | 2 +- plugins/setoid_ring/ArithRing.v | 2 +- plugins/setoid_ring/BinList.v | 2 +- plugins/setoid_ring/Cring.v | 2 +- plugins/setoid_ring/Field.v | 2 +- plugins/setoid_ring/Field_tac.v | 2 +- plugins/setoid_ring/Field_theory.v | 2 +- plugins/setoid_ring/InitialRing.v | 2 +- plugins/setoid_ring/NArithRing.v | 2 +- plugins/setoid_ring/Ncring.v | 2 +- plugins/setoid_ring/Ncring_initial.v | 2 +- plugins/setoid_ring/Ncring_polynom.v | 2 +- plugins/setoid_ring/Ncring_tac.v | 2 +- plugins/setoid_ring/Ring.v | 2 +- plugins/setoid_ring/Ring_base.v | 2 +- plugins/setoid_ring/Ring_polynom.v | 2 +- plugins/setoid_ring/Ring_theory.v | 2 +- plugins/setoid_ring/ZArithRing.v | 2 +- plugins/setoid_ring/newring.ml4 | 2 +- plugins/subtac/eterm.mli | 2 +- plugins/subtac/g_subtac.ml4 | 2 +- plugins/subtac/subtac.ml | 2 +- plugins/subtac/subtac_cases.ml | 6 +-- plugins/subtac/subtac_cases.mli | 2 +- plugins/subtac/subtac_classes.ml | 2 +- plugins/subtac/subtac_classes.mli | 2 +- plugins/subtac/subtac_coercion.ml | 8 +-- plugins/subtac/subtac_pretyping.ml | 4 +- plugins/subtac/subtac_pretyping_F.ml | 25 +++++----- plugins/syntax/nat_syntax.ml | 2 +- plugins/syntax/numbers_syntax.ml | 2 +- plugins/syntax/r_syntax.ml | 2 +- plugins/syntax/z_syntax.ml | 2 +- plugins/xml/dumptree.ml4 | 2 +- 163 files changed, 282 insertions(+), 231 deletions(-) (limited to 'plugins') diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 1c021eee..056ae3a9 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* (t, l) | Construct _ -> (t,l) @@ -576,7 +576,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = onLastHypId (fun heq_id -> tclTHENLIST [ (* Then the new hypothesis *) tclMAP introduction_no_check dyn_infos.rec_hyps; - (* observe_tac "after_introduction" *)(fun g' -> + observe_tac "after_introduction" (fun g' -> (* We get infos on the equations introduced*) let new_term_value_eq = pf_type_of g' (mkVar heq_id) in (* compute the new value of the body *) @@ -603,7 +603,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos = } in clean_goal_with_heq ptes_infos continue_tac new_infos g' - )]) + )]) ] g diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 6b6e4838..ffaa2208 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* + match pat with + | Genarg.IntroIdentifier id -> add id acc + | _ -> anomaly "Not an identifier" + ) + (List.nth intro_pats (pred i)) + empty + in let prove_branche i g = (* We get the identifiers of this branch *) - let this_branche_ids = - List.fold_right - (fun (_,pat) acc -> - match pat with - | Genarg.IntroIdentifier id -> Idset.add id acc - | _ -> anomaly "Not an identifier" - ) - (List.nth intro_pats (pred i)) - Idset.empty - in (* and get the real args of the branch by unfolding the defined constant *) let pre_args,pre_tac = List.fold_right (fun (id,b,t) (pre_args,pre_tac) -> - if Idset.mem id this_branche_ids + if Idset.mem id (this_branche_ids Idset.empty Idset.add i) then match b with - | None -> (id::pre_args,pre_tac) + | None -> + (id::pre_args,pre_tac) | Some b -> (pre_args, tclTHEN (h_reduce (Glob_term.Unfold([Glob_term.all_occurrences_expr,EvalVarRef id])) allHyps) pre_tac @@ -347,8 +351,8 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem when (eq_constr eq eq_ind) && array_exists (eq_constr graph') graphs_constr -> - ((mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|])) - ::args.(2)::acc) + ((mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|])) + ::args.(2)::acc) | _ -> mkVar hid :: acc end | _ -> mkVar hid :: acc @@ -390,7 +394,7 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem | [res;hres] -> res,hres | _ -> assert false in - observe (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor); + observe_tac_msg (str "constructor := " ++ Printer.pr_lconstr_env (pf_env g) app_constructor) ( tclTHENSEQ [ @@ -455,11 +459,10 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem fun g -> observe (pr_constr_with_binding (Printer.pr_lconstr_env (pf_env g)) (mkVar principle_id,bindings)); - functional_induction false (applist(funs_constr.(i),List.map mkVar args_names)) - (Some (mkVar principle_id,bindings)) - pat g + h_apply false false [dummy_loc,(mkVar principle_id,bindings)] g )) - (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g ) + (fun i g -> observe_tac ("proving branche "^string_of_int i) + (tclTHEN (tclMAP h_intro (this_branche_ids [] (fun a b -> a::b) i)) (prove_branche i)) g ) ] g diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml index bd1a1710..e1f10be2 100644 --- a/plugins/funind/merge.ml +++ b/plugins/funind/merge.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* let (f,_) = decompose_app t in eq_constr f (well_founded ()) - | _ -> assert false + | _ -> false in let compare t1 t2 = let b1,b2= is_well_founded t1,is_well_founded t2 in diff --git a/plugins/micromega/CheckerMaker.v b/plugins/micromega/CheckerMaker.v index fa780671..04336747 100644 --- a/plugins/micromega/CheckerMaker.v +++ b/plugins/micromega/CheckerMaker.v @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* = 8.5, this option is set by default. +*) + let read f () = !f let write f x = f:=x @@ -81,6 +98,14 @@ let _ = optread = read old_style_flag; optwrite = write old_style_flag } +let _ = + declare_bool_option + { optsync = true; + optdepr = false; + optname = "Omega automatic reset of generated names"; + optkey = ["Stable";"Omega"]; + optread = read reset_flag; + optwrite = write reset_flag } let all_time = timing "Omega " let solver_time = timing "Solver " @@ -89,30 +114,35 @@ let elim_time = timing "Elim " let simpl_time = timing "Simpl " let generalize_time = timing "Generalize" +let intref, reset_all_references = + let refs = ref [] in + (fun n -> let r = ref n in refs := (r,n) :: !refs; r), + (fun () -> List.iter (fun (r,n) -> r:=n) !refs) + let new_identifier = - let cpt = ref 0 in + let cpt = intref 0 in (fun () -> let s = "Omega" ^ string_of_int !cpt in incr cpt; id_of_string s) let new_identifier_state = - let cpt = ref 0 in + let cpt = intref 0 in (fun () -> let s = make_ident "State" (Some !cpt) in incr cpt; s) let new_identifier_var = - let cpt = ref 0 in + let cpt = intref 0 in (fun () -> let s = "Zvar" ^ string_of_int !cpt in incr cpt; id_of_string s) let new_id = - let cpt = ref 0 in fun () -> incr cpt; !cpt + let cpt = intref 0 in fun () -> incr cpt; !cpt let new_var_num = - let cpt = ref 1000 in (fun () -> incr cpt; !cpt) + let cpt = intref 1000 in (fun () -> incr cpt; !cpt) let new_var = - let cpt = ref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt) + let cpt = intref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt) let display_var i = Printf.sprintf "X%d" i -let intern_id,unintern_id = +let intern_id,unintern_id,reset_intern_tables = let cpt = ref 0 in let table = Hashtbl.create 7 and co_table = Hashtbl.create 7 in (fun (name : identifier) -> @@ -124,7 +154,8 @@ let intern_id,unintern_id = (fun idx -> try Hashtbl.find co_table idx with Not_found -> let v = new_var () in - Hashtbl.add table v idx; Hashtbl.add co_table idx v; v) + Hashtbl.add table v idx; Hashtbl.add co_table idx v; v), + (fun () -> cpt := 0; Hashtbl.clear table) let mk_then = tclTHENLIST @@ -141,19 +172,28 @@ let rev_assoc k = in loop -let tag_hypothesis,tag_of_hyp, hyp_of_tag = +let tag_hypothesis,tag_of_hyp, hyp_of_tag, clear_tags = let l = ref ([]:(identifier * int) list) in (fun h id -> l := (h,id):: !l), (fun h -> try List.assoc h !l with Not_found -> failwith "tag_hypothesis"), - (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis") + (fun h -> try rev_assoc h !l with Not_found -> failwith "tag_hypothesis"), + (fun () -> l := []) -let hide_constr,find_constr,clear_tables,dump_tables = +let hide_constr,find_constr,clear_constr_tables,dump_tables = let l = ref ([]:(constr * (identifier * identifier * bool)) list) in (fun h id eg b -> l := (h,(id,eg,b)):: !l), (fun h -> try list_assoc_f eq_constr h !l with Not_found -> failwith "find_contr"), (fun () -> l := []), (fun () -> !l) +let reset_all () = + if !reset_flag then begin + reset_all_references (); + reset_intern_tables (); + clear_tags (); + clear_constr_tables () + end + (* Lazy evaluation is used for Coq constants, because this code is evaluated before the compiled modules are loaded. To use the constant Zplus, one must type "Lazy.force coq_Zplus" @@ -1388,7 +1428,7 @@ let reintroduce id = tclTHEN (tclTRY (clear [id])) (intro_using id) let coq_omega gl = - clear_tables (); + clear_constr_tables (); let tactic_normalisation, system = List.fold_left (destructure_omega gl) ([],[]) (pf_hyps_types gl) in let prelude,sys = @@ -1814,6 +1854,7 @@ let destructure_goal = all_time (destructure_goal) let omega_solver gl = Coqlib.check_required_library ["Coq";"omega";"Omega"]; + reset_all (); let result = destructure_goal gl in (* if !display_time_flag then begin text_time (); flush Pervasives.stdout end; *) diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4 index 1542b60c..b2a5b5dc 100644 --- a/plugins/omega/g_omega.ml4 +++ b/plugins/omega/g_omega.ml4 @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* - let (evd',j) = Coercion.inh_conv_coerce_to loc env !isevars j p in + let (evd',j) = Coercion.inh_conv_coerce_to true loc env !isevars j p in isevars := evd'; j | None -> j diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli index 91142067..5ef42b13 100644 --- a/plugins/subtac/subtac_cases.mli +++ b/plugins/subtac/subtac_cases.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* anomaly "apply_coercion" - let inh_app_fun env isevars j = + let inh_app_fun _ env isevars j = let isevars = ref isevars in let t = hnf env !isevars j.uj_type in match kind_of_term t with @@ -481,8 +481,8 @@ module Coercion = struct | Some (init, cur) -> (evd, cj) - let inh_conv_coerce_to = inh_conv_coerce_to_gen false - let inh_conv_coerce_rigid_to = inh_conv_coerce_to_gen true + let inh_conv_coerce_to _ = inh_conv_coerce_to_gen false + let inh_conv_coerce_rigid_to _ = inh_conv_coerce_to_gen true let inh_conv_coerces_to loc env isevars t ((abs, t') as _tycon) = let nabsinit, nabs = diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml index fac6b567..68636574 100644 --- a/plugins/subtac/subtac_pretyping.ml +++ b/plugins/subtac/subtac_pretyping.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* j - | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to loc env) evdref j t + | Some t -> evd_comb2 (Coercion.inh_conv_coerce_to resolve_tc loc env) evdref j t let push_rels vars env = List.fold_right push_rel vars env @@ -188,11 +188,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct (* [pretype tycon env evdref lvar lmeta cstr] attempts to type [cstr] *) (* in environment [env], with existential variables [( evdref)] and *) (* the type constraint tycon *) - let rec pretype (tycon : type_constraint) env evdref lvar c = + let rec pretype resolve_tc (tycon : type_constraint) env evdref lvar c = (* let _ = try Subtac_utils.trace (str "pretype " ++ Subtac_utils.my_print_glob_constr env c ++ *) (* str " with tycon " ++ Evarutil.pr_tycon env tycon) *) (* with _ -> () *) (* in *) + let pretype = pretype resolve_tc in + let pretype_type = pretype_type resolve_tc in + let inh_conv_coerce_to_tycon = inh_conv_coerce_to_tycon resolve_tc in match c with | GRef (loc,ref) -> inh_conv_coerce_to_tycon loc env evdref @@ -335,7 +338,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct | [] -> resj | c::rest -> let argloc = loc_of_glob_constr c in - let resj = evd_comb1 (Coercion.inh_app_fun env) evdref resj in + let resj = evd_comb1 (Coercion.inh_app_fun resolve_tc env) evdref resj in let resty = whd_betadeltaiota env !evdref resj.uj_type in match kind_of_term resty with | Prod (na,c1,c2) -> @@ -557,7 +560,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct inh_conv_coerce_to_tycon loc env evdref cj tycon (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *) - and pretype_type valcon env evdref lvar = function + and pretype_type resolve_tc valcon env evdref lvar = function | GHole loc -> (match valcon with | Some v -> @@ -577,7 +580,7 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct { utj_val = e_new_evar evdref env ~src:loc (mkSort s); utj_type = s}) | c -> - let j = pretype empty_tycon env evdref lvar c in + let j = pretype resolve_tc empty_tycon env evdref lvar c in let loc = loc_of_glob_constr c in let tj = evd_comb1 (Coercion.inh_coerce_to_sort loc env) evdref j in match valcon with @@ -592,9 +595,9 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let c' = match kind with | OfType exptyp -> let tycon = match exptyp with None -> empty_tycon | Some t -> mk_tycon t in - (pretype tycon env evdref lvar c).uj_val + (pretype resolve_classes tycon env evdref lvar c).uj_val | IsType -> - (pretype_type empty_valcon env evdref lvar c).utj_val + (pretype_type resolve_classes empty_valcon env evdref lvar c).utj_val in if resolve_classes then (try @@ -616,14 +619,14 @@ module SubtacPretyping_F (Coercion : Coercion.S) = struct let understand_judgment sigma env c = let evdref = ref (create_evar_defs sigma) in - let j = pretype empty_tycon env evdref ([],[]) c in + let j = pretype true empty_tycon env evdref ([],[]) c in let evd = consider_remaining_unif_problems env !evdref in let j = j_nf_evar evd j in check_evars env sigma evd (mkCast(j.uj_val,DEFAULTcast, j.uj_type)); j let understand_judgment_tcc evdref env c = - let j = pretype empty_tycon env evdref ([],[]) c in + let j = pretype true empty_tycon env evdref ([],[]) c in j_nf_evar !evdref j (* Raw calls to the unsafe inference machine: boolean says if we must diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml index 63b44008..2899f17f 100644 --- a/plugins/syntax/nat_syntax.ml +++ b/plugins/syntax/nat_syntax.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(*