diff options
| -rw-r--r-- | contrib/field/Field.v | 5 | ||||
| -rw-r--r-- | contrib/field/Field_Tactic.v | 207 | ||||
| -rw-r--r-- | contrib/field/field.ml4 | 40 | ||||
| -rw-r--r-- | parsing/g_ltac.ml4 | 5 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 4 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 1 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 | ||||
| -rw-r--r-- | proofs/tacinterp.ml | 30 | ||||
| -rw-r--r-- | toplevel/command.mli | 8 | ||||
| -rw-r--r-- | toplevel/mltop.ml4 | 8 |
10 files changed, 258 insertions, 51 deletions
diff --git a/contrib/field/Field.v b/contrib/field/Field.v index eb82846d7..69687c100 100644 --- a/contrib/field/Field.v +++ b/contrib/field/Field.v @@ -35,7 +35,8 @@ with vernac : ast := $ainv_l ($LIST $l))]. Grammar tactic simple_tactic: ast := - | field [ "Field" ] -> [(Field)]. + | field [ "Field" constrarg_list($arg) ] -> [(Field ($LIST $arg))]. Syntax tactic level 0: - | field [(Field)] -> ["Field"]. + | field [ <<(Field ($LIST $lc))>> ] -> ["Field" [1 1] (LISTSPC ($LIST $lc))] + | field_e [(Field)] -> ["Field"]. diff --git a/contrib/field/Field_Tactic.v b/contrib/field/Field_Tactic.v index c3002a552..a18d87f0a 100644 --- a/contrib/field/Field_Tactic.v +++ b/contrib/field/Field_Tactic.v @@ -19,17 +19,17 @@ Recursive Tactic Definition MemAssoc var lvar := | [(nilT ?)] -> false | [(consT ? ?1 ?2)] -> (Match ?1==var With - | [?1== ?1] -> true + | [?1==?1] -> true | _ -> (MemAssoc var ?2)). Recursive Tactic Definition SeekVarAux FT lvar trm := - Let AT = Eval Compute in (A FT) - And AzeroT = Eval Compute in (Azero FT) - And AoneT = Eval Compute in (Aone FT) - And AplusT = Eval Compute in (Aplus FT) - And AmultT = Eval Compute in (Amult FT) - And AoppT = Eval Compute in (Aopp FT) - And AinvT = Eval Compute in (Ainv FT) In + Let AT = Eval Cbv Beta Delta [A] Iota in (A FT) + And AzeroT = Eval Cbv Beta Delta [Azero] Iota in (Azero FT) + And AoneT = Eval Cbv Beta Delta [Aone] Iota in (Aone FT) + And AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT) + And AmultT = Eval Cbv Beta Delta [Amult] Iota in (Amult FT) + And AoppT = Eval Cbv Beta Delta [Aopp] Iota in (Aopp FT) + And AinvT = Eval Cbv Beta Delta [Ainv] Iota in (Ainv FT) In Match trm With | [(AzeroT)] -> lvar | [(AoneT)] -> lvar @@ -48,7 +48,7 @@ Recursive Tactic Definition SeekVarAux FT lvar trm := | [(false)] -> '(consT AT ?1 lvar). Tactic Definition SeekVar FT trm := - Let AT = Eval Compute in (A FT) In + Let AT = Eval Cbv Beta Delta [A] Iota in (A FT) In (SeekVarAux FT '(nilT AT) trm). Recursive Tactic Definition NumberAux lvar cpt := @@ -72,14 +72,14 @@ Recursive Tactic Definition Assoc elt lst := | [?1== ?1] -> ?2 | _ -> (Assoc elt ?3). -Recursive Tactic Definition interp_A FT lvar trm := - Let AT = Eval Compute in (A FT) - And AzeroT = Eval Compute in (Azero FT) - And AoneT = Eval Compute in (Aone FT) - And AplusT = Eval Compute in (Aplus FT) - And AmultT = Eval Compute in (Amult FT) - And AoppT = Eval Compute in (Aopp FT) - And AinvT = Eval Compute in (Ainv FT) In +Recursive Meta Definition interp_A FT lvar trm := + Let AT = Eval Cbv Beta Delta [A] Iota in (A FT) + And AzeroT = Eval Cbv Beta Delta [Azero] Iota in (Azero FT) + And AoneT = Eval Cbv Beta Delta [Aone] Iota in (Aone FT) + And AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT) + And AmultT = Eval Cbv Beta Delta [Amult] Iota in (Amult FT) + And AoppT = Eval Cbv Beta Delta [Aopp] Iota in (Aopp FT) + And AinvT = Eval Cbv Beta Delta [Ainv] Iota in (Ainv FT) In Match trm With | [(AzeroT)] -> EAzero | [(AoneT)] -> EAone @@ -169,20 +169,25 @@ Tactic Definition GrepMult := Match Context With | [ id: ~(interp_ExprA ? ? ?)== ? |- ?] -> id. +Tactic Definition WeakReduce := + Match Context With + | [|-[(interp_ExprA ?1 ?2 ?)]] -> + Cbv Beta Delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list ?1 ?2 A + Azero Aone Aplus Amult Aopp Ainv] Zeta Iota. + Tactic Definition Multiply mul := Match Context With | [|-(interp_ExprA ?1 ?2 ?3)==(interp_ExprA ?1 ?2 ?4)] -> - Let AzeroT = Eval Compute in (Azero ?1) In + Let AzeroT = Eval Cbv Beta Delta [Azero ?1] Iota in (Azero ?1) In Cut ~(interp_ExprA ?1 ?2 mul)==AzeroT; [Intro; Let id = GrepMult In - Apply (mult_eq ?1 ?3 ?4 mul ?2 id)(*; - Cbv Beta Delta -[interp_ExprA] Zeta Iota*) - |Cbv Beta Delta -[not] Zeta Iota; - Let AmultT = Eval Compute in (Amult ?1) - And AoneT = Eval Compute in (Aone ?1) In - (Match Context With - | [|-[(AmultT ? AoneT)]] -> Rewrite (AmultT_1r ?1));Clear ?1 ?2]. + Apply (mult_eq ?1 ?3 ?4 mul ?2 id) + |WeakReduce; + Let AoneT = Eval Cbv Beta Delta [Aone ?1] Iota in (Aone ?1) + And AmultT = Eval Cbv Beta Delta [Amult ?1] Iota in (Amult ?1) In + Try (Match Context With + | [|-[(AmultT ? AoneT)]] -> Rewrite (AmultT_1r ?1));Clear ?1 ?2]. Tactic Definition ApplyMultiply FT lvar trm := Cut (interp_ExprA FT lvar (multiply trm))==(interp_ExprA FT lvar trm); @@ -210,10 +215,10 @@ Tactic Definition ApplyInverse mul FT lvar trm := Tactic Definition StrongFail tac := First [tac|Fail 2]. Tactic Definition InverseTestAux FT trm := - Let AplusT = Eval Compute in (Aplus FT) - And AmultT = Eval Compute in (Amult FT) - And AoppT = Eval Compute in (Aopp FT) - And AinvT = Eval Compute in (Ainv FT) In + Let AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT) + And AmultT = Eval Cbv Beta Delta [Amult] Iota in (Amult FT) + And AoppT = Eval Cbv Beta Delta [Aopp] Iota in (Aopp FT) + And AinvT = Eval Cbv Beta Delta [Ainv] Iota in (Ainv FT) In Match trm With | [(AinvT ?)] -> Fail 1 | [(AoppT ?1)] -> StrongFail (InverseTestAux FT ?1) @@ -224,7 +229,7 @@ Tactic Definition InverseTestAux FT trm := | _ -> Idtac. Tactic Definition InverseTest FT := - Let AplusT = Eval Compute in (Aplus FT) In + Let AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT) In Match Context With | [|- ?1==?2] -> (InverseTestAux FT '(AplusT ?1 ?2)). @@ -246,9 +251,18 @@ Tactic Definition Unfolds FT := | [(Some ? ?1)] -> Unfold ?1 | _ -> Idtac). -Tactic Definition Field_Gen FT := - Let AplusT = Eval Compute in (Aplus FT) In - Unfolds FT; +Tactic Definition Reduce FT := + Let AzeroT = Eval Cbv Beta Delta [Azero] Iota in (Azero FT) + And AoneT = Eval Cbv Beta Delta [Aone] Iota in (Aone FT) + And AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT) + And AmultT = Eval Cbv Beta Delta [Amult] Iota in (Amult FT) + And AoppT = Eval Cbv Beta Delta [Aopp] Iota in (Aopp FT) + And AinvT = Eval Cbv Beta Delta [Ainv] Iota in (Ainv FT) In + Cbv Beta Delta -[AzeroT AoneT AplusT AmultT AoppT AinvT] Zeta Iota + Orelse Compute. + +Tactic Definition Field_Gen_Aux FT := + Let AplusT = Eval Cbv Beta Delta [Aplus] Iota in (Aplus FT) In Match Context With | [|- ?1==?2] -> Let lvar = (BuildVarList FT '(AplusT ?1 ?2)) In @@ -260,5 +274,128 @@ Tactic Definition Field_Gen FT := |Intros;(ApplySimplif ApplyDistrib);(ApplySimplif ApplyAssoc); (Multiply mul);[(ApplySimplif ApplyMultiply); (ApplySimplif (ApplyInverse mul)); - (Let id = GrepMult In Clear id);Compute; - First [(InverseTest FT);Ring|Clear ft vm;(Field_Gen FT)]|Idtac]]. + (Let id = GrepMult In Clear id);WeakReduce;Clear ft vm; + First [(InverseTest FT);Ring|(Field_Gen_Aux FT)]|Idtac]]. + +Tactic Definition Field_Gen FT := + Unfolds FT;((InverseTest FT);Ring) Orelse (Field_Gen_Aux FT). + +(*****************************) +(* Term Simplification *) +(*****************************) + +(**** Minus and division expansions ****) + +Meta Definition InitExp FT trm := + Let e = + (Match Eval Cbv Beta Delta [Aminus] Iota in (Aminus FT) With + | [(Some ? ?1)] -> Eval Cbv Beta Delta [?1] in trm + | _ -> trm) In + Match Eval Cbv Beta Delta [Adiv] Iota in (Adiv FT) With + | [(Some ? ?1)] -> Eval Cbv Beta Delta [?1] in e + | _ -> e. + +(**** Inverses simplification ****) + +Recursive Meta Definition SimplInv trm:= + Match trm With + | [(EAplus ?1 ?2)] -> + Let e1 = (SimplInv ?1) + And e2 = (SimplInv ?2) In + '(EAplus e1 e2) + | [(EAmult ?1 ?2)] -> + Let e1 = (SimplInv ?1) + And e2 = (SimplInv ?2) In + '(EAmult e1 e2) + | [(EAopp ?1)] -> Let e = (SimplInv ?1) In '(EAopp e) + | [(EAinv ?1)] -> (SimplInvAux ?1) + | [?1] -> ?1 +And SimplInvAux trm := + Match trm With + | [(EAinv ?1)] -> (SimplInv ?1) + | [(EAmult ?1 ?2)] -> + Let e1 = (SimplInv '(EAinv ?1)) + And e2 = (SimplInv '(EAinv ?2)) In + '(EAmult e1 e2) + | [?1] -> Let e = (SimplInv ?1) In '(EAinv e). + +(**** Monom simplification ****) + +Recursive Meta Definition Map fcn lst := + Match lst With + | [(nilT ?)] -> lst + | [(consT ?1 ?2 ?3)] -> + Let r = (fcn ?2) + And t = (Map fcn ?3) In + '(consT ?1 r t). + +Recursive Meta Definition BuildMonomAux lst trm := + Match lst With + | [(nilT ?)] -> Eval Compute in (assoc trm) + | [(consT ? ?1 ?2)] -> BuildMonomAux ?2 '(EAmult trm ?1). + +Recursive Meta Definition BuildMonom lnum lden := + Let ildn = (Map (Fun e -> '(EAinv e)) lden) In + Let ltot = Eval Compute in (appT ExprA lnum ildn) In + Let trm = (BuildMonomAux ltot EAone) In + Match trm With + | [(EAmult ? ?1)] -> ?1 + | [?1] -> ?1. + +Recursive Meta Definition SimplMonomAux lnum lden trm := + Match trm With + | [(EAmult (EAinv ?1) ?2)] -> + Let mma = (MemAssoc ?1 lnum) In + (Match mma With + | [true] -> + Let newlnum = (Remove ?1 lnum) In SimplMonomAux newlnum lden ?2 + | [false] -> SimplMonomAux lnum '(consT ExprA ?1 lden) ?2) + | [(EAmult ?1 ?2)] -> + Let mma = (MemAssoc ?1 lden) In + (Match mma With + | [true] -> + Let newlden = (Remove ?1 lden) In SimplMonomAux lnum newlden ?2 + | [false] -> SimplMonomAux '(consT ExprA ?1 lnum) lden ?2) + | [(EAinv ?1)] -> + Let mma = (MemAssoc ?1 lnum) In + (Match mma With + | [true] -> + Let newlnum = (Remove ?1 lnum) In BuildMonom newlnum lden + | [false] -> BuildMonom lnum '(consT ExprA ?1 lden)) + | [?1] -> + Let mma = (MemAssoc ?1 lden) In + (Match mma With + | [true] -> + Let newlden = (Remove ?1 lden) In BuildMonom lnum newlden + | [false] -> BuildMonom '(consT ExprA ?1 lnum) lden). + +Meta Definition SimplMonom trm := + SimplMonomAux '(nilT ExprA) '(nilT ExprA) trm. + +Recursive Meta Definition SimplAllMonoms trm := + Match trm With + | [(EAplus ?1 ?2)] -> + Let e1 = (SimplMonom ?1) + And e2 = (SimplAllMonoms ?2) In + '(EAplus e1 e2) + | [?1] -> SimplMonom ?1. + +(**** Associativity and distribution ****) + +Meta Definition AssocDistrib trm := Eval Compute in (assoc (distrib trm)). + +(**** The tactic Field_Term ****) + +Tactic Definition EvalWeakReduce trm := + Eval Cbv Beta Delta [interp_ExprA assoc_2nd eq_nat_dec mult_of_list A Azero + Aone Aplus Amult Aopp Ainv] Zeta Iota in trm. + +Tactic Definition Field_Term FT exp := + Let newexp = (InitExp FT exp) In + Let lvar = (BuildVarList FT newexp) In + Let trm = (interp_A FT lvar newexp) In + Let tma = Eval Compute in (assoc trm) In + Let tsmp = (SimplAllMonoms (AssocDistrib (SimplAllMonoms + (SimplInv tma)))) In + Let trep = (EvalWeakReduce '(interp_ExprA FT lvar tsmp)) In + Replace exp with trep;[Ring trep|Field_Gen FT]. diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4 index 10e22b86c..1edf302e0 100644 --- a/contrib/field/field.ml4 +++ b/contrib/field/field.ml4 @@ -11,10 +11,12 @@ (* $Id$ *) open Names +open Pp open Proof_type open Tacinterp open Tacmach open Term +open Typing open Util open Vernacinterp @@ -77,7 +79,10 @@ let add_field a aplus amult aone azero aopp aeq ainv aminus_o adiv_o rth with | UserError("Add Semi Ring",_) -> ()); let th = mkApp ((constant ["Field_Theory"] "Build_Field_Theory"), [|a;aplus;amult;aone;azero;aopp;aeq;ainv;aminus_o;adiv_o;rth;ainv_l|]) in - Lib.add_anonymous_leaf (in_addfield (a,th)) + begin + let _ = type_of (Global.env ()) Evd.empty th in (); + Lib.add_anonymous_leaf (in_addfield (a,th)) + end end (* Vernac command declaration *) @@ -128,5 +133,36 @@ let field g = | [id:t |- ?] -> Rewrite id;Reflexivity)|Field_Gen FT] | [|- (eqT ? ? ?)] -> Field_Gen FT>>) g +(* Verifies that all the terms have the same type and gives the right theory *) +let guess_theory env evc = function + | c::tl -> + let t = type_of env evc c in + if List.exists (fun c1 -> + not (Reductionops.is_conv env evc t (type_of env evc c1))) tl then + errorlabstrm "Field:" (str" All the terms must have the same type") + else + lookup t + | [] -> anomaly "Field: must have a non-empty constr list here" + +(* Guesses the type and calls Field_Term with the right theory *) +let field_term l g = + let env = (pf_env g) + and evc = (project g) in + let th = constrIn (guess_theory env evc l) + and nl = List.map constrIn (Quote.sort_subterm g l) in + (List.fold_right + (fun c a -> + let tac = (Tacinterp.interp <:tactic<(Field_Term $th $c)>>) in + tclTHENSI tac [a]) nl tclIDTAC) g + +(* Gives the constr list from the tactic_arg list *) +let targ_constr = + List.map + (fun e -> + match e with + | Constr c -> c + | _ -> anomaly "Field: must be a constr") + (* Declaration of Field *) -let _ = hide_tactic "Field" (function _ -> field) +let _ = hide_tactic "Field" + (fun l -> if l = [] then field else field_term (targ_constr l)) diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index a64ebb826..b90924f81 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -21,7 +21,7 @@ open Util (* Tactics grammar rules *) GEXTEND Gram - GLOBAL: tactic_expr input_fun; + GLOBAL: tactic_atom tactic_atom0 tactic_expr input_fun; input_fun: [ [ l = identarg -> l | "()" -> <:ast< (VOID) >> ] ] @@ -144,7 +144,8 @@ GEXTEND Gram | IDENT "Inst"; id = identarg; "["; c = Constr.constr; "]" -> <:ast< (COMMAND (CONTEXT $id $c)) >> | st = simple_tactic -> st - | id = lqualid; la = LIST1 tactic_atom0 -> <:ast< (APP $id ($LIST $la)) >> + | id = lqualid; la = LIST1 tactic_atom0 -> + <:ast< (APP $id ($LIST $la)) >> | id = lqualid -> id | ta = tactic_atom0 -> ta ] ] ; diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 0c2a61896..a864227a7 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -51,7 +51,7 @@ END (* Gallina declarations *) GEXTEND Gram - GLOBAL: gallina gallina_ext thm_tok theorem_body; + GLOBAL: gallina gallina_ext reduce thm_tok theorem_body; theorem_body_line: [ [ n = numarg; ":"; tac = tacarg; "." -> @@ -105,7 +105,7 @@ GEXTEND Gram ; reduce: [ [ IDENT "Eval"; r = Tactic.red_tactic; "in" -> - [ <:ast< (TACTIC_ARG (REDEXP $r)) >> ] + [ <:ast< (TACTIC_ARG (REDEXP $r)) >> ] | -> [] ] ] ; binders_list: diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index ffa82f034..c45c8227d 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -371,6 +371,7 @@ module Vernac_ = let constrarg = gec "constrarg" let ne_constrarg_list = gec_list "ne_constrarg_list" let tacarg = gec "tacarg" + let reduce = gec_list "reduce" let sortarg = gec "sortarg" let theorem_body = gec "theorem_body" let thm_tok = gec "thm_tok" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 3b55171b7..781c65162 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -181,6 +181,7 @@ module Vernac_ : val constrarg : Coqast.t Gram.Entry.e val ne_constrarg_list : Coqast.t list Gram.Entry.e val tacarg : Coqast.t Gram.Entry.e + val reduce : Coqast.t list Gram.Entry.e val sortarg : Coqast.t Gram.Entry.e val theorem_body : Coqast.t Gram.Entry.e val thm_tok : Coqast.t Gram.Entry.e diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml index dfefece60..f84266a1d 100644 --- a/proofs/tacinterp.ml +++ b/proofs/tacinterp.ml @@ -105,14 +105,25 @@ let make_ids ast = function | _ -> anomalylabstrm "make_ids" (str "Not an identifier") (* Gives Qualid's and makes the possible injection identifier -> qualid *) -let make_qid = function +(*let make_qid = function | VArg (Qualid _) as arg -> arg | VArg (Identifier id) -> VArg (Qualid (make_short_qualid id)) | VArg (Constr c) -> (match (kind_of_term c) with | Const cst -> VArg (Qualid (qualid_of_sp cst)) | _ -> anomalylabstrm "make_qid" (str "Not a Qualid")) - | _ -> anomalylabstrm "make_qid" (str "Not a Qualid") + | _ -> anomalylabstrm "make_qid" (str "Not a Qualid")*) + +(* Gives qualid's and makes the possible injection identifier -> qualid *) +let make_qid = function + | VArg (Qualid q) -> q + | VArg (Identifier id) -> make_short_qualid id + | VArg (Constr c) -> + (match (kind_of_term c) with + | Const cst -> qualid_of_sp cst + | Var id -> make_short_qualid id + | _ -> anomalylabstrm "make_qid" (str "Not a qualid")) + | _ -> anomalylabstrm "make_qid" (str "Not a qualid") (* Transforms a named_context into a (string * constr) list *) let make_hyps = List.map (fun (id,_,typ) -> (string_of_id id,body_of_type typ)) @@ -520,10 +531,10 @@ let rec val_interp ist ast = with | Not_found -> (try (vcontext_interp ist (lookup s)) with | Not_found -> VArg (Identifier s))) - | Node(_,"QUALIDARG",[Nvar(_,s)]) -> + (* | Node(_,"QUALIDARG",[Nvar(_,s)]) -> (try (make_qid (unrec (List.assoc s ist.lfun))) with | Not_found -> - VArg (Qualid (qid_interp ist ast))) + VArg (Qualid (qid_interp ist ast)))*) | Node(_,"QUALIDARG",_) | Node(_,"QUALIDMETA",_) -> VArg (Qualid (qid_interp ist ast)) | Str(_,s) -> VArg (Quoted_string s) @@ -1064,9 +1075,16 @@ and cast_opencom_interp ist com = (* Interprets a qualified name. This can be a metavariable to be injected *) and qid_interp ist = function - | Node(loc,"QUALIDARG",p) -> interp_qualid p + | Node(_,"QUALIDARG",p) -> + (match p with + | [Nvar(_,s)] -> + (try (make_qid (unrec (List.assoc s ist.lfun))) + with | Not_found -> interp_qualid p) + | _ -> interp_qualid p) | Node(loc,"QUALIDMETA",[Num(_,n)]) -> - Nametab.qualid_of_sp (destConst(List.assoc n ist.lmatch)) + (try Nametab.qualid_of_sp (destConst (List.assoc n ist.lmatch)) with + | Invalid_argument "destConst" -> + make_qualid (make_dirpath []) (destVar (List.assoc n ist.lmatch))) | ast -> anomaly_loc (Ast.loc ast, "Tacinterp.qid_interp",(str "Unrecognizable qualid ast: " ++ print_ast ast)) diff --git a/toplevel/command.mli b/toplevel/command.mli index 04ae5a454..baa983788 100644 --- a/toplevel/command.mli +++ b/toplevel/command.mli @@ -21,6 +21,14 @@ open Nametab functions of [Declare]; they return an absolute reference to the defined object *) +val constant_entry_of_com : + Coqast.t * Coqast.t option * bool -> Safe_typing.constant_entry + +val declare_global_definition : + Names.identifier -> + Safe_typing.constant_entry -> + Declare.strength -> bool -> Nametab.global_reference + val definition_body : identifier -> bool * strength -> Coqast.t -> Coqast.t option -> global_reference diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4 index d9325a2e7..0b86c7656 100644 --- a/toplevel/mltop.ml4 +++ b/toplevel/mltop.ml4 @@ -97,12 +97,16 @@ let dir_ml_load s = match !load with | WithTop t -> if is_in_path !coq_mlpath_copy s then - try t.load_obj s + try + t.load_obj s with - | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u + | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> + raise u | _ -> errorlabstrm "Mltop.load_object" [< str"Cannot link ml-object "; str s; str" to Coq code." >] + + else errorlabstrm "Mltop.load_object" [< str"File not found on loadpath : "; str s >] |