diff options
| author | corbinea | 2003-07-03 05:53:12 +0000 |
|---|---|---|
| committer | corbinea | 2003-07-03 05:53:12 +0000 |
| commit | 3bf1c17402769a3b400a8a063303c4844915f022 (patch) | |
| tree | fac16221f7e9d2175259cf32762e8262e7ed72b7 /contrib/first-order/rules.ml | |
| parent | b94378923370c90eb336a21e94ad48405ccfdfbc (diff) | |
addition of Auto hints in Ground
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4217 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/first-order/rules.ml')
| -rw-r--r-- | contrib/first-order/rules.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/first-order/rules.ml b/contrib/first-order/rules.ml index ad36bc4d70..bd69262906 100644 --- a/contrib/first-order/rules.ml +++ b/contrib/first-order/rules.ml @@ -39,10 +39,10 @@ let wrap n b continue seq gls= List.exists (occur_var_in_decl env id) ctx then (aux (i-1) q (nd::ctx)) else - add_formula false (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in + add_formula Hyp (VarRef id) typ (aux (i-1) q (nd::ctx)) gls in let seq1=aux n nc [] in let seq2=if b then - add_formula true dummy_id (pf_concl gls) seq1 gls else seq1 in + add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in continue seq2 gls let id_of_global=function |