diff options
| author | herbelin | 2001-10-05 14:49:48 +0000 |
|---|---|---|
| committer | herbelin | 2001-10-05 14:49:48 +0000 |
| commit | 8dbab7f463cabfc2913ab8615973c96ac98bf371 (patch) | |
| tree | 4be620fad92be1173cf2ba1865d3568e1d143d2c | |
| parent | b35f7449426057e962d5646a216dbc63df33a046 (diff) | |
Petit oubli à propos de ThinBody
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2105 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | proofs/logic.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 38f2d1d0fc..22751eaf9d 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -643,6 +643,9 @@ let prim_extractor subfun vl pft = (* No need to make ids Anonymous in vl: subst_vars take the more recent *) subfun vl pf + | {ref=Some(Prim{name=ThinBody;hypspecs=ids},[pf])} -> + subfun vl pf + | {ref=Some(Prim{name=Move _;hypspecs=ids},[pf])} -> subfun vl pf @@ -715,6 +718,9 @@ let pr_prim_rule = function | {name=Thin;hypspecs=ids} -> [< 'sTR"Clear " ; prlist_with_sep pr_spc pr_id ids >] + | {name=ThinBody;hypspecs=ids} -> + [< 'sTR"ClearBody " ; prlist_with_sep pr_spc pr_id ids >] + | {name=Move withdep;hypspecs=[id1;id2]} -> [< 'sTR (if withdep then "Dependent " else ""); 'sTR"Move " ; pr_id id1; 'sTR " after "; pr_id id2 >] |