diff options
| author | corbinea | 2006-09-20 17:18:18 +0000 |
|---|---|---|
| committer | corbinea | 2006-09-20 17:18:18 +0000 |
| commit | 0f4f723a5608075ff4aa48290314df30843efbcb (patch) | |
| tree | 09316ca71749b9218972ca801356388c04d29b4c /tactics/auto.ml | |
| parent | c6b9d70f9292fc9f4b5f272b5b955af0e8fe0bea (diff) | |
Declarative Proof Language: main commit
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9154 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 1ecb29f7e4..d1caa98625 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -192,7 +192,10 @@ let make_exact_entry (c,cty) = { pri=0; pat=None; code=Give_exact c }) let dummy_goal = - {it={evar_hyps=empty_named_context_val;evar_concl=mkProp;evar_body=Evar_empty}; + {it={evar_hyps=empty_named_context_val; + evar_concl=mkProp; + evar_body=Evar_empty; + evar_extra=None}; sigma=Evd.empty} let make_apply_entry env sigma (eapply,verbose) (c,cty) = |