diff options
| author | msozeau | 2008-06-06 22:39:43 +0000 |
|---|---|---|
| committer | msozeau | 2008-06-06 22:39:43 +0000 |
| commit | a1fe45ddbd37d3c447a23cde0ee21f105ef42ac0 (patch) | |
| tree | 648a977d3137ffa9c7cc97e8503c0a5d8620dbfa /tactics | |
| parent | 0cdfa2fb137989f75cdebfa3a64726bc0d56a8af (diff) | |
Enhancements to coqdoc, better globalization of sections and modules.
Minor fix in Morphisms which prevented working with higher-order
morphisms and PER relations.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11065 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index e9424ed0c4..e41bebea11 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -432,16 +432,17 @@ let add_hints local dbnames0 h = add_trivials env sigma (List.map f lhints) local dbnames | HintsUnfold lhints -> let f r = - let r = Syntax_def.global_with_alias r in - let r' = match r with + let gr = Syntax_def.global_with_alias r in + let r' = match gr with | ConstRef c -> EvalConstRef c | VarRef c -> EvalVarRef c | _ -> errorlabstrm "evalref_of_ref" - (str "Cannot coerce" ++ spc () ++ pr_global r ++ spc () ++ + (str "Cannot coerce" ++ spc () ++ pr_global gr ++ spc () ++ str "to an evaluable reference") in - (r,r') in + if !Flags.dump then Constrintern.add_glob (loc_of_reference r) gr; + (gr,r') in add_unfolds (List.map f lhints) local dbnames | HintsConstructors lqid -> let add_one qid = |