diff options
| author | gregoire | 2005-12-02 10:01:15 +0000 |
|---|---|---|
| committer | gregoire | 2005-12-02 10:01:15 +0000 |
| commit | bf578ad5e2f63b7a36aeaef5e0597101db1bd24a (patch) | |
| tree | c0bc4e5f9ae67b8a03b28134dab3dcfe31d184dd /contrib/xml/xmlcommand.ml | |
| parent | 825a338a1ddf1685d55bb5193aa5da078a534e1c (diff) | |
Changement des named_context
Ajout de cast indiquant au kernel la strategie a suivre
Resolution du bug sur les coinductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7639 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml/xmlcommand.ml')
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index e8f149402d..96f73abe0e 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -290,7 +290,7 @@ let find_hyps t = | T.Meta _ | T.Evar _ | T.Sort _ -> l - | T.Cast (te,ty) -> aux (aux l te) ty + | T.Cast (te,_, ty) -> aux (aux l te) ty | T.Prod (_,s,t) -> aux (aux l s) t | T.Lambda (_,s,t) -> aux (aux l s) t | T.LetIn (_,s,_,t) -> aux (aux l s) t @@ -359,7 +359,7 @@ let mk_current_proof_obj is_a_variable id bo ty evar_map env = (* t will not be exported to XML. Thus no unsharing performed *) final_var_ids,(n, Acic.Def (Unshare.unshare b',t))::tl' in - aux [] (List.rev evar_hyps) + aux [] (List.rev (Environ.named_context_of_val evar_hyps)) in (* We map the named context to a rel context and every Var to a Rel *) (n,context,Unshare.unshare (Term.subst_vars final_var_ids evar_concl)) |