Meilleure gestion de la reduction dans Field

Field term (nouveau)
Injections dans l'interpreteur de tactiques
Exportation de quelques entrees de grammaires
Exportation de quelques fonctionnalites des definitions


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2538 85f007b7-540e-0410-9357-904b9bb8a0f7

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 >]