diff options
| author | herbelin | 2001-06-25 13:37:10 +0000 |
|---|---|---|
| committer | herbelin | 2001-06-25 13:37:10 +0000 |
| commit | 8ed67d4a2dabe40186c8ad0550fb3fbd2d9b8787 (patch) | |
| tree | 08a302bdd28b98df9da11751b831229ffc21cc04 /proofs/proof_trees.ml | |
| parent | 77259e0b563a10d57b55ac38400ca1843fb938f3 (diff) | |
Les réduction dans les hypothèses s'appliquent maintenant au corps de la définition en cas de LetIn (l'horrible syntaxe 'Unfold toto in (Type of hyp)' permet de forcer la réduction dans le type
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/proof_trees.ml')
| -rw-r--r-- | proofs/proof_trees.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml index 18cd475cde..45fe9e5a47 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.ml @@ -407,7 +407,11 @@ let ast_of_cvt_arg = function | Constr_context _ -> anomalylabstrm "ast_of_cvt_arg" [<'sTR "Constr_context argument could not be used">] - | Clause idl -> ope ("CLAUSE", List.map (compose nvar string_of_id) idl) + | Clause idl -> + let transl = function + | InHyp id -> ope ("INHYP", [nvar (string_of_id id)]) + | InHypType id -> ope ("INHYPTYPE", [nvar (string_of_id id)]) in + ope ("CLAUSE", List.map transl idl) | Bindings bl -> ope ("BINDINGS", List.map (ast_of_cvt_bind (fun x -> x)) bl) | Cbindings bl -> |